$\forall$$A$:MsgA. AtomFree(da($A$)) $\Rightarrow$ ($\forall$$k$:Knd. AtomFree(Type;$A$.da($k$)))